\begin{tabbing}
prior{-}state($f$;${\it base}$;$X$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if $e$ $\in_{b}$ prior($X$)\+
\\[0ex]then $f$(prior{-}state($f$;${\it base}$;$X$;prior($X$)($e$)),$X$(prior($X$)($e$)))
\\[0ex]else ${\it base}$
\\[0ex]fi 
\\[0ex]
\-\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]es{-}local{-}prior{-}state\=\{i:l\}\+
\\[0ex](${\it es}$; $f$; ${\it base}$; $X$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if $e$ $\in_{b}$ es{-}prior{-}interface\{i:l\}(${\it es}$; $X$)\+
\\[0ex]then \=$f$\+
\\[0ex](es{-}local{-}prior{-}state\=\{i:l\}\+
\\[0ex](${\it es}$; $f$; ${\it base}$; $X$; es{-}prior{-}interface\{i:l\}(${\it es}$; $X$)($e$))
\-\\[0ex],$X$(es{-}prior{-}interface\=\{i:l\}\+
\\[0ex](${\it es}$; $X$)($e$)))
\-\-\\[0ex]else ${\it base}$
\\[0ex]fi 
\-\\[0ex]\emph{(recursive)}
\end{tabbing}